Lean Finder V2: Semantic Search for Mathlib That Disambiguates User Queries
Lean Finder V2：面向 Mathlib 的语义搜索与查询消歧
🧭 语义搜索 · 查询改写与消歧
Simon Fraser University · Rice University · University of Pittsburgh
用对抗训练生成大规模短歧义查询，结合模型微调与输入层改写，在 MathlibQR 上至少相对提升 11%
📌 工作参考价值（4 点）
- 用对抗训练补足“短歧义 query”数据：电商搜索里“苹果”“nike 卫衣”等短查询经常缺 context；可仿照用生成模型 + 判别器迭代生成大量带标签的歧义 query，而不是只靠真实日志，显著扩充训练集，解决数据稀疏。
- 模型层 + 输入层双层消歧：同时 fine-tune 检索模型（增强对短 query 的鲁棒性）并在检索前对 query 做改写/补全（如加类目、属性、别名），两者互补；在商品搜索或 Agent 工具检索中可分开评估增量，避免只做单一层。
- 面向真实短查询做人类评估基准：构建少量人工标注的短 query benchmark，用 unlabeled 真实 human/agent 交互做 ranking 评估，比离线 dense retrieval 指标更贴近线上体验。
- 检索质量直接挂钩下游 agent 任务成功率：与 Claude Code 集成后证明 proof success 提升，说明 Agent 工具检索/商品召回改善能直接转化为任务成功；建议将检索召回作为 Agent 流程中的关键优化点。